COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00026 00003	.skip 1
C00027 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.CB FORMALIZATION OF TWO PUZZLES INVOLVING KNOWLEDGE


	This paper describes a formal system and uses it to
express the puzzle of the three wise men and the puzzle of Mr. S
and Mr. P.  Four innovations in the axiomatization of knowledge
were required: the ability to express joint knowledge of several
people, the ability to express the initial non-knowledge,
the ability to describe knowing what rather than merely knowing that,
and the ability to express the change which occurs when someone
learns something.  Our axioms are written in first order logic
and use Kripke-style possible worlds directly rather than modal
operators or imitations thereof.  We intend to use functions
imitating modal operators and taking "propositions" and "individual
concepts" as operands, but we haven't yet solved the problem
of how to treat learning in such a formalism.

	The puzzles to be treated are the following:

.bb The three wise men

	%2"A certain king wishes to test his three wise men.  He
arranges them in a circle so that they can see and hear each other and tells
them that he will put a white or black spot on each of their foreheads
but that at least one spot will be white.  In fact all three spots
are white.  He then repeatedly asks them, "Do you know the cclor of
your spot".  What do they answer?"%1

	The solution is that they answer, %2"No"%1, the first two
times the question is asked and answer %2"Yes"%1 thereafter.

	This is a variant form of the puzzle.  The traditional form
is

	%2"A certain king wishes to determine which of his three
wise men is the wisest.  He
arranges them in a circle so that they can see and hear each other and tells
them that he will put a white or black spot on each of their foreheads
but that at least one spot will be white.  In fact all three spots
are white.  He then offers his favor to the one who will first tell
him the color of his spot.  After a while, the wisest announces
that his spot his white.  How does he know?"%1

	The intended solution is that the wisest reasons that if
his spot were black, the second would see a black and a white and
would reason that if his spot were black, the third would have seen
two black spot and reasoned from the king's announcement that his
spot was white.  This traditional version  requires
the wise men to reason about how fast their colleagues reason, and
we don't wish to try to formalize this.

.bb Mr. S and Mr. P

	%2Two numbers ⊗m and ⊗n are chosen such that 2_≤_m_≤_n_≤_99.
Mr. S is told their sum and Mr. P is told their product.  The following
dialogue ensues:

%2Mr. P:	I don't know the numbers.

%2Mr. S:	I knew you didn't know.  I don't know either.

%2Mr. P:	Now I know the numbers.

%2Mr. S:	Now I know them too.

%2In view of the above dialogue, what are the numbers?"%1


.bb Simple axiomatization of the wise men

	If we can assume that the first and second wisemen don't
know the colors of their spots, that the second knows that the
first doesn't know, and the third knows this, then a simple
axiomatization that doesn't explicitly treat learning works.

[In this draft, we omit this section.  Instead we include an
older self-contained memo written when this was our main approach
to the problem].


.bb Full axiomatization of the wise men

	The axioms are given in a form acceptable to FOL, the proof
checker computer program for an extended first order logic at the
Stanford Artificial Intelligence Laboratory.  FOL uses a sorted
logic and constants and variables are declared to have given sorts,
and quantifiers on these variables are interpreted as ranging over
the sorts corresponding to the variables.

	The axiomatization has the following features:
.item←0
	#. It is entirely in first order logic rather than in a modal
logic.

	#. The Kripke accessibility relation is axiomatized.  No knowledge
operator or function is used.  We hope to present a second axiomatization
using a knowledge function, but we haven't yet decided how to handle time
and learning in such an axiomatization.

	#. We are essentially treating "knowing what" rather than "knowing
that".  We say that p knows the color of his spot in world w by saying
that in all worlds accessible from w, the color of the spot is the same
as in w.

	#. We treat learning by giving the accessibility relation a time
parameter.  To say that someone learns something is done by saying that
the worlds accessible to him at time n+1 are the subset of those accessible
at time n in which the something is true.

	#. The problems treated are complicated by the need to treat
joint knowledge and joint learning.  This is done by introducing
fictitious persons who know what a group of people know jointly.

.nofill

declare INDCONST RW ε WORLD;
declare INDVAR w w1 w2 w3 w4 w5 ε WORLD;
.fill

	RW denotes the real world, and w, w1, ... , w5 are variables
ranging over worlds.

declare INDVAR m n m1 m2 m3 n1 n2 n3 ε NATNUM;

	We use natural numbers for times.

.nofill

declare INDCONST W1 W2 W3 W123 ε PERSON;
declare INDVAR p p0 p1 p2 ε PERSON;
.fill

	W1, W2 and W3 are the three wisemen.  W123 is a fictitious person
who knows whatever W1, W2 and W3 know jointly.  The joint knowledge of several
people is typified by events that occur in their joint presence.  Not only do
they all know it, but W1 knows that W2 knows that W1 knows that W3 knows etc.
Instead of introducing W123, we could introduce prefixes of like "W1
knows that W2 knows" as objects and quantify over prefixes.

declare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);

	This Kripke-style accessibility relation has two more arguments than
is usual in modal logic - a person and a time.

.nofill

declare INDVAR c c1 c2 c3 c4 ε COLORS;
declare INDCONST W B ε COLORS;
.fill

	There are two colors - white and black.

declare OPCONST color(PERSON,WORLD) = COLORS;

	A person has a color in a world.  Note that the previous
axiomatization was simpler.  We merely had three propositions WISE1, WISE2
and WISE3 asserting that the respective wise men had white spots.  We need
the colors, because we want to quantify over colors.

axiom reflex:	∀w p m.A(w,w,p,m);;

	The accessibility relation is reflexive as is usual in Kripke the
semantics of M.

axiom transitive:	∀w1 w2 w3 p m.(A(w1,w2,p,m) ∧ A(w2,w3,p,m) ⊃ A(w1,w3,p,m));;

	Making the accessibility relation transitive gives an S4 like system.
We use transitivity in the proof, but we aren't sure it is necessary.

axiom who:	∀p.(p=W1 ∨ p=W2 ∨ p=W3 ∨ p=W123);;

	We need to delimit the set of wise men.

axiom w123:	∀w1 w2 m.(A(w1,w2,W1,m) ∨ A(w1,w2,W2,m) ∨ A(w1,w2,W3,m)
⊃ A(w1,w2,W123,m));;

	This says that anything the wise men know jointly, they
know individually.

axiom foolspot:	∀w.(color(W123,w)=W);;

	This ad hoc axiom is the penalty for introducing W123 as an
ordinary individual whose spot must therefore have a color.  It would have
been better to distinguish between real persons with spots and the
fictitious person(s) who only know things.  Anyway, we give W123 a white
spot and make it generally known, e.g. true in all possible worlds.

.nofill

axiom color:	¬(W=B)
		∀c.(c=W ∨ c=B)
;;
.fill

	Both of these axioms about the colors are used in the proof.

axiom rw:	color(W1,RW) = W ∧ color(W2,RW) = W ∧ color(W3,RW) = W;;

	In fact all spots are white.

axiom king:	∀w.(A(RW,w,W123,0) ⊃ color(W1,w)=W ∨ color(W2,w)=W
∨ color(W3,w)=W);;

	They jointly know that at least one spot is white, since
the king stated it in their mutual presence.  We use the consequence
that W3 knows that W2 knows that W1 knows this fact.

.nofill

axiom initial:	∀c w.(A(RW,w,W123,0) ⊃
	(c=W ∨ color(W2,w)=W ∨ color(W3,w)=W
		⊃ ∃w1.(A(w,w1,W1,0) ∧ color(W1,w1) = c)) ∧
	(c=W ∨ color(W1,w)=W ∨ color(W3,w)=W
		⊃ ∃w1.(A(w,w1,W2,0) ∧ color(W2,w1) = c)) ∧
	(c=W ∨ color(W1,w)=W ∨ color(W2,w)=W
		⊃ ∃w1.(A(w,w1,W3,0) ∧ color(W3,w1) = c)))
.fill

	∀w w1.(A(RW,w,W123,0) ∧ A(w,w1,W1,0)
⊃ color(W2,w1) = color(W2,w) ∧ color(W3,w1) = color(W3,w))

	∀w w1.(A(RW,w,W123,0) ∧ A(w,w1,W2,0)
⊃ color(W1,w1) = color(W1,w) ∧ color(W3,w1) = color(W3,w))

	∀w w1.(A(RW,w,W123,0) ∧ A(w,w1,W3,0)
 color(W1,w1) = color(W1,w) ∧ color(W2,w1) = color(W2,w))
;;

	These are actually four axioms.  The last three say that every one
knows that each knows the colors of the other men's spots.
The first part says that they all know that no-one knows anything
more than what he can see and what the king told them.  We establish
non-knowledge by asserting the existence of enough possible worlds.
The ability to quantify over colors is convenient for expressing this axiom
in a natural way.  In the S and P problem it is essential, because
we would otherwise need a conjunction of 4753 terms.

axiom elwek1:	∀w.(A(RW,w,W123,1) ≡ A(RW,w,W123,0) ∧
∀p.(∀w1.(A(w,w1,p,0) ⊃ color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,0)
⊃ color(p,w1)=color(p,RW))))

	∀w1 w2.(A(w1,w2,W1,1) ≡ A(w1,w2,W1,0) ∧ A(w1,w2,W123,1))

	∀w1 w2.(A(w1,w2,W2,1) ≡ A(w1,w2,W2,0) ∧ A(w1,w2,W123,1))

	∀w1 w2.(A(w1,w2,W3,1) ≡ A(w1,w2,W3,0) ∧ A(w1,w2,W123,1))
;;

	This axiom and the next one are the same except that one
deals with the transition from time 0 to time 1 and the other deals
with the transition from time 1 to time 2.
Each says that
they jointly learn who (if anyone) knows the color of his spot.  The
quantifier ∀p in this axiom covers W123 also and forced us to say
that they jointly know the color of W123's spot.

axiom elwek2:	∀w.(A(RW,w,W123,2) ≡ A(RW,w,W123,1) ∧
∀p.(∀w1.(A(w,w1,p,1) ⊃ color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,1)
⊃ color(p,w1)=color(p,RW))))

	∀w1 w2.(A(w1,w2,W1,2) ≡ A(w1,w2,W1,1) ∧ A(w1,w2,W123,1))

	∀w1 w2.(A(w1,w2,W2,2) ≡ A(w1,w2,W2,1) ∧ A(w1,w2,W123,1))

	∀w1 w2.(A(w1,w2,W3,2) ≡ A(w1,w2,W3,1) ∧ A(w1,w2,W123,1))
;;

	The file WISEMA.PRF[S78,JMC] at the Stanford AI Lab contains
a computer checked proof from these axioms of

∀w.(A(RW,w,W3,2) ⊃ color(W3,w) = color(W3,RW))

which is the assertion that at time 2, the third wise man knows the
color of his spot.  As intermediate results we had to prove that
previous to time 2, the other wise men did not know the colors of
their spots.  In this symmetrical axiomatization, we could have made
the proof with a variable wise man instead of the constant W3.


.bb "Axiomatization of Mr. S and Mr. P"

	These axioms involve the same ideas as the second wise man
axiomatization.  In fact, we derived them first.

.nofill

declare INDCONST m0 n0 ε NATNUM;
declare INDVAR m n m1 m2 m3 n1 n2 n3 ε NATNUM;

declare INDCONST RW ε WORLD;
declare INDVAR w w1 w2 w3 ε WORLD;

declare OPCONST M(WORLD) = NATNUM;
declare OPCONST N(WORLD) = NATNUM;

declare INDCONST S P SP ε PERSON;
declare INDVAR s s0 s1 s2 ε PERSON;

declare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);
declare PREDCONST ok(NATNUM,NATNUM);

declare PREDCONST agree(WORLD,WORLD);

declare PREDPAR phi(WORLD,WORLD);

COMMENT : The predicate agree is used to abbreviate subsequent axioms. :

axiom agree:	∀w1 w2.(agree(w1,w2) ≡ M(w1) = M(w2) ∧ N(w1) = N(w2));;

axiom reflex:	∀w s m.A(w,w,s,m);;

axiom transitive:	∀w1 w2 w3 s m.(A(w1,w2,s,m) ∧ A(w2,w3,s,m) ⊃ A(w1,w3,s,m));;

COMMENT : The axiom sp characterizes the fictious person SP as knowing
what S and P know jointly, i.e. S knows that P knows that S knows, etc. :

axiom sp:	∀w1 w2 m.(A(w1,w2,S,m) ∨ A(w1,w2,P,m) ⊃ A(w1,w2,SP,m))

		∀m.(
		∀w1 w2.(A(w1,w2,S,m) ∨ A(w1,w2,P,m) ⊃ phi(w1,w2)) ∧
		∀w1 w2 w3.(phi(w1,w2) ∧ phi(w2,w3) ⊃ phi(w1,w3))
⊃	∀w1 w2.(phi(w1,w2) ⊃ A(w1,w2,SP,m)))
;;


axiom rw:	m0 = M(RW)
		n0 = N(RW)
;;

axiom ok:	∀m n.(ok(m,n) ≡ 1<m ∧ 1<n ∧ m≤n ∧ m<100 ∧ n<100)
		∀w.ok(M(w),N(w))
;;

COMMENT : initial establishes the existence of enough possible worlds
to express that S and P initially know only what follows from their
knowledge of the sum and product respectively, and that they jointly
know this ignorance. :

axiom initial:
	∀w w1.(A(RW,w,SP,0) ∧ A(w,w1,S,0) ⊃ M(w1)+N(w1) = M(w)+N(w))
	∀w w1.(A(RW,w,SP,0) ∧ A(w,w1,P,0) ⊃ M(w1)*N(w1) = M(w)*N(w))
	∀w m n.(A(RW,w,SP,0) ∧ ok(m,n) ∧ M(w) + N(w) = m + n ⊃
∃w1.(A(w,w1,S,0) ∧ M(w1) = m ∧ N(w1) = n))
	∀w m n.(A(RW,w,SP,0) ∧ ok(m,n) ∧ M(w) * N(w) = m * n ⊃
∃w1.(A(w,w1,P,0) ∧ M(w1) = m ∧ N(w1) = n))
;;

COMMENT : Mr. P doesn't know the numbers. :

axiom npk:
	∃w.(A(RW,w,P,0) ∧ ¬agree(RW,w))
;;

COMMENT : Mr. S knew that Mr. P didn't know. :

axiom sknpk:
	∀w.(A(RW,w,S,0) ⊃ ∃w1.(A(w,w1,P,0) ∧ ¬agree(w,w1)))
;;

COMMENT : Mr. S doesn't know either. :

axiom nsk:
	∃w.(A(RW,w,S,0) ∧ ¬agree(RW,w))
;;

COMMENT : They jointly learn that Mr. S knows that Mr. P doesn't know and
that Mr. S doesn't know either. :

axiom elsknpkansk:
	∀w.(A(RW,w,SP,1) ≡ A(RW,w,SP,0) ∧ 
∀w1.(A(w,w1,S,0) ⊃ ∃w2.(A(w1,w2,P,0) ∧ ¬agree(w1,w2))) ∧
∃w1.(A(w,w1,S,0) ∧ ¬agree(w,w1)))

	∀w1 w2.(A(w1,w2,S,1) ≡ A(w1,w2,S,0) ∧ A(w1,w2,SP,1))

	∀w1 w2.(A(w1,w2,P,1) ≡ A(w1,w2,P,0) ∧ A(w1,w2,SP,1))
;;

COMMENT : In this new situation, Mr. P knows the numbers. :

axiom pk:
	∀w.(A(RW,w,P,1) ⊃ agree(RW,w))
;;

COMMENT : Everyone learns that Mr. P now knows. :

axiom elpk:
	∀w.(A(RW,w,SP,2) ≡ A(RW,w,SP,1)
∧ ∀w1.(A(w,w1,P,1) ⊃ agree(w,w1)))

	∀w1 w2.(A(w1,w2,S,2) ≡ A(w1,w2,S,1) ∧ A(w1,w2,SP,2))

	∀w1 w2.(A(w1,w2,P,2) ≡ A(w1,w2,P,1) ∧ A(w1,w2,SP,2))
;;

COMMENT : In this new situation Mr. S knows too. :

axiom sk:	∀w.(A(RW,w,S,2) ⊃ agree(RW,w));;
	
COMMENT : The following are purely arithmetic definitions and are intended
to be used in expressing the translation of the problem from the
modal form to a purely arithmetic form.  Completing the proof
that m0 = 4 and n0 = 13 will require
using a set of axioms for arithmetic, but that is not of interest here :

declare PREDCONST R0(NATNUM,NATNUM) R1(NATNUM,NATNUM)
R2(NATNUM,NATNUM) R3(NATNUM,NATNUM);

axiom R0:	∀m n.(R0(m,n) ≡ ok(m,n) ∧ ∃m1 n1.(ok(m1,n1) ∧ m1*n1 = m*n
∧ ¬(m1=m ∧ n1=n)))
;;

axiom R1:	∀m n.(R1(m,n) ≡ ok(m,n) ∧
			∀m1 n1.(ok(m1,n1) ∧ m1+n1 = m+n ⊃ R0(m1,n1)) ∧
			∃m1 n1.(m1+n1 = m+n ∧ ¬(m1=m ∧ n1=n)));;


axiom R2:	∀m n.(R2(m,n) ≡ ok(m,n) ∧ 
			∀m1 n1.(m1*n1 = m*n ∧ R1(m1,n1) ⊃ m1=m ∧ n1=n));;

axiom R3:	∀m n.(R3(m,n) ≡ ok(m,n) ∧
			∀m1 n1.(m1+n1 = m+n ∧ R2(m1,n1) ⊃ m1=m ∧ n1=n));;

.fill

	We should be able to prove %2R3(m0,n0)%1 from the above axioms.
The subsequent proof that %2m0_=_4_∧_n0_=_13%1 should not involve the
knowledge axioms and should be purely arithmetic.

	There may still be a bug in the S and P axioms, since the proof
has not been carried out on the computer.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of
KNOW[E78,JMC]
PUBbed at {time} on {date}.%1